\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, ${\it ks}$:Knd List,\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]$\neg$$x$ $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$A$:Realizer.\+
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ $\neg$R{-}has{-}loc($A$;$i$)
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. isrcv($k$) $\Rightarrow$ R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ Valtype(${\it da}$;$k$))
\\[0ex]$\Rightarrow$ ($\forall$$k$$\in$${\it ks}$. $k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$) $\parallel$ $A$)
\-
\end{tabbing}